\begin{tabbing}
ecl{-}halt(${\it ds}$;${\it da}$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=ecl\_ind($x$;$k$,${\it test}$.$\lambda$$n$,$L$. $n$ $=$ 0\+
\\[0ex]\& (\=$\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List, $s$:State(${\it ds}$), $v$:Valtype(${\it da}$;$k$).\+
\\[0ex]$L$ $=$ (${\it L'}$ @ [$\langle$$k$$,\,$$s$$,\,$$v$$\rangle$]) \& ${\it test}$($s$,$v$)
\\[0ex]\& ($\forall$$t$$\in$${\it L'}$. $\neg$let ${\it k'}$,$s$,$v$ = $t$ in $k$ $=$ ${\it k'}$ \& ${\it test}$($s$,$v$)));$a$,$b$,${\it ha}$,${\it hb}$.$\lambda$$n$,$L$. 0$<$$n$ \& ${\it ha}$($n$,$L$)
\-\\[0ex]$\vee$ (\=$\exists$$L_{1}$, $L_{2}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]$L$ $=$ ($L_{1}$ @ $L_{2}$) \& ${\it ha}$(0,$L_{1}$) \& ${\it hb}$($n$,$L_{2}$));$a$,$b$,${\it ha}$,${\it hb}$.$\lambda$$n$,$L$.
\-\\[0ex](\=$n$ $=$ 0\+
\\[0ex]$\Rightarrow$ \=${\it ha}$(0,$L$) \& ($\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ \& ${\it hb}$(0,${\it L'}$))\+
\\[0ex]$\vee$ ${\it hb}$(0,$L$) \& ($\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ \& ${\it ha}$(0,${\it L'}$)))
\-\-\\[0ex]\& (\=0$<$$n$\+
\\[0ex]$\Rightarrow$ \=${\it ha}$($n$,$L$) \& ($\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\Rightarrow$ ${\it hb}$($m$,${\it L'}$) $\Rightarrow$ ${\it L'}$ $=$ $L$ \& $n$$\leq$$m$)\+
\\[0ex]$\vee$ \=${\it hb}$($n$,$L$)\+
\\[0ex]\& (\=$\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L'}$ $\leq$ $L$ $\Rightarrow$ ${\it ha}$($m$,${\it L'}$) $\Rightarrow$ ${\it L'}$ $=$ $L$ \& $n$$\leq$$m$));$a$,$b$,${\it ha}$,${\it hb}$.$\lambda$$n$,$L$. ${\it ha}$($n$,$L$)
\-\-\-\-\\[0ex]\& ($\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\Rightarrow$ ${\it hb}$($m$,${\it L'}$) $\Rightarrow$ ${\it L'}$ $=$ $L$ \& $n$$\leq$$m$)
\\[0ex]$\vee$ \=${\it hb}$($n$,$L$)\+
\\[0ex]\& ($\forall$$m$:$\mathbb{N}$, ${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ $\Rightarrow$ ${\it ha}$($m$,${\it L'}$) $\Rightarrow$ ${\it L'}$ $=$ $L$ \& $n$$\leq$$m$);$a$,${\it ha}$.$\lambda$$n$,$L$.
\-\\[0ex]0$<$$n$ \& star{-}append(event{-}info(${\it ds}$;${\it da}$);${\it ha}$(0);${\it ha}$($n$))($L$);$a$,$m$,${\it ha}$.${\it ha}$;$a$,$m$,${\it ha}$.$\lambda$$n$,$L$. 0$<$$n$
\\[0ex]\& ${\it ha}$($n$,$L$)
\\[0ex]$\vee$ $n$ $=$ $m$ \& ${\it ha}$(0,$L$);$a$,$l$,${\it ha}$.$\lambda$$n$,$L$. ${\it ha}$($n$,$L$) \& $\neg$($n$ $\in$ $l$) $\vee$ $n$ $=$ 0 \& ($\exists$$m$$\in$$l$.${\it ha}$($m$,$L$)))
\-
\end{tabbing}